<html>
<head>
<title>Skolemization Relations</title>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
<STYLE TYPE="text/css">
<!--
P { margin-top:7px; margin-bottom:8px; }
-->
</STYLE>
</head>

<body bgcolor="#FFFFFF" text="#000000">

<h2>private namespace</h2>

<p>
A new reserved keyword "private" has been added for declaring a sig, fun, pred, field, or an entire imported module
as being "private" to this module (and does not show up in the namespace of other modules that import this module).
</p>

<h2>Example 1: private sig, private field, private function, and private predicate</h2>

<table border=1 cellpadding=2 cellspacing=2>

<tr valign=top>

<td>
<pre>
  module moduleA

  open moduleB
</pre>
</td>

<td>
<pre>
  module moduleB

  sig Person {
      favorite: Book,
      knows: set Person,
      private likes: set Person
  }

  private sig Book { year: Int }

  fun allBook: set Book { Book }

  private fun union[a, b: set univ]: set univ { a+b }
</pre>
</td>

</tr>

</table>

<p>
From moduleA, you can refer to "Person", "favorite", "knows", and "allBook".
<br>
You cannot refer to "likes" because it is a private field, and you cannot refer
to "union" because it is a private function.
</p>

<p>
From moduleA, you cannot refer to "Book" since it is a private sig,
<br>
and you cannot refer to "year" because it is a field in a private sig (and thus
it is automatically private).
</p>

<p>
The important thing to note here is this is purely a namespace management mechanism, and you may still
be able to access these "hidden" values via other names. For example, if you have Person X, you can access
X.favorite to see the Book atom corresponding to his favorite book, even though you cannot refer to the Book signature
by name. Likewise, you can get every atom in the Book sig by calling the "allBook" function.
</p>

<h2>Example 2: private open</h2>

<table border=1 cellpadding=2 cellspacing=2>

<tr valign=top>

<td>
<pre>
  module moduleA

  open moduleB
</pre>
</td>

<td>
<pre>
  module moduleB

  private open moduleC

  open moduleD

  sig B { }
</pre>
</td>

<td>
<pre>
  module moduleC

  sig C { }
</pre>
</td>

<td>
<pre>
  module moduleD

  sig D { }
</pre>
</td>

</tr>

</table>

<p>In moduleB, you can certainly refer to B, C, and D.</p>

<p>In moduleA, you can refer to B and D, but you cannot refer to C,
since moduleB imported moduleC as a "private import".</p>

</body></html>
